<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>Theorem</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="Theorem";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Theorem.html" target="_top">Frames</a></li>
<li><a href="Theorem.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#fields_inherited_from_class_mmj.lang.Assrt">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class Theorem" class="title">Class Theorem</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">mmj.lang.MObj</a></li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">mmj.lang.Stmt</a></li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">mmj.lang.Assrt</a></li>
<li>
<ul class="inheritance">
<li>mmj.lang.Theorem</li>
</ul>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">Theorem</span>
extends <a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a></pre>
<div class="block">Theorem corresponds to a Metamath "$p" statement, AKA, a
 "provable assertion".
 <p>
 Theorem is distinguished from Axiom by having a... proof, as well as an
 OptFrame (Optional Frame).
 <p>
 A Metamath "proof" is simply an array of Stmt labels, which in mmj equates to
 <code>Stmt[]</code>. The proof is in RPN, Reverse Polish Notation format and when
 fed into the Proof Verifier engine recreates the Theorem's Formula -- that's
 all a "proof" is, assuming it follows the "rules". See Metamath.pdf and
 mmj.verify.VerifyProofs.java for more info.
 <p>
 The proof need not be complete, and may consist of nothing but a "?" step in
 the source file -- which is stored as a <code>null</code> proof step in mmj.
 Non-missing Proof steps must refer to "active" Hyp's or Assrt's with Stmt.seq
 < Theorem.seq. Verification of a proof is not performed within Theorem --
 that is handled by mmj.verify.VerifyProofs (in theory, Proof Verification
 could be performed at this time, but since most proofs are static and the
 Proof Verification process is very CPU intensive, normal Metamath practice is
 to verify proofs only when the user requests it.)
 <p>
 An OptFrame consists of those Hyp's and DjVars that are "in scope" but are
 not present in the the MandFrame (Mandatory Frame). Together the OptFrame and
 MandFrame comprise what Metamath.pdf terms the "Extended Frame".
 <p>
 (As a side note, the "validity" of a proof has nothing to do with the Theorem
 being reference-able by subsequent Theorems' proofs. Nor does Metamath
 formally require that every LogHyp in scope be referenced within a Theorem's
 proof. A warning message could be presented for the latter situation, but has
 not yet been coded.)</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.Assrt">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a></h3>
<code><a href="../../mmj/lang/Assrt.html#logHypArray">logHypArray</a>, <a href="../../mmj/lang/Assrt.html#mandFrame">mandFrame</a>, <a href="../../mmj/lang/Assrt.html#NBR_LOG_HYP_SEQ">NBR_LOG_HYP_SEQ</a>, <a href="../../mmj/lang/Assrt.html#sortedLogHypArray">sortedLogHypArray</a>, <a href="../../mmj/lang/Assrt.html#varHypArray">varHypArray</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.Stmt">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></h3>
<code><a href="../../mmj/lang/Stmt.html#DESC_NBR_PROOF_REFS">DESC_NBR_PROOF_REFS</a>, <a href="../../mmj/lang/Stmt.html#exprParseTree">exprParseTree</a>, <a href="../../mmj/lang/Stmt.html#LABEL">LABEL</a>, <a href="../../mmj/lang/Stmt.html#logHypsL1HiLoKey">logHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#logHypsMaxDepth">logHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#nbrProofRefs">nbrProofRefs</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#chapterNbr">chapterNbr</a>, <a href="../../mmj/lang/MObj.html#description">description</a>, <a href="../../mmj/lang/MObj.html#isTempObject">isTempObject</a>, <a href="../../mmj/lang/MObj.html#SECTION_AND_MOBJ_NBR">SECTION_AND_MOBJ_NBR</a>, <a href="../../mmj/lang/MObj.html#sectionMObjNbr">sectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#sectionNbr">sectionNbr</a>, <a href="../../mmj/lang/MObj.html#seq">seq</a>, <a href="../../mmj/lang/MObj.html#SEQ">SEQ</a></code></li>
</ul>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/Theorem.html#Theorem(int, java.util.List, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.mmio.BlockList, mmj.lang.ProofCompression, mmj.lang.Messages)">Theorem</a></strong>(int&nbsp;seq,
       java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;scopeDefList,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
       java.lang.String&nbsp;labelS,
       java.lang.String&nbsp;typS,
       java.util.List&lt;java.lang.String&gt;&nbsp;symList,
       java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
       <a href="../../mmj/mmio/BlockList.html" title="class in mmj.mmio">BlockList</a>&nbsp;proofBlockList,
       <a href="../../mmj/lang/ProofCompression.html" title="class in mmj.lang">ProofCompression</a>&nbsp;proofCompression,
       <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Construct Theorem using the entire enchilada from mmj.mmio.SrcStmt.java
 including compressed proof blocks.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/Theorem.html#Theorem(int, java.util.List, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.lang.Messages)">Theorem</a></strong>(int&nbsp;seq,
       java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;scopeDefList,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
       java.lang.String&nbsp;labelS,
       java.lang.String&nbsp;typS,
       java.util.List&lt;java.lang.String&gt;&nbsp;symList,
       java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
       <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Construct Theorem using the entire enchilada from mmj.mmio.SrcStmt.java,
 plus a few condiments.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#editProofListDefAndActive(java.util.Map, java.util.List)">editProofListDefAndActive</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
                         java.util.List&lt;java.lang.String&gt;&nbsp;proofList)</code>
<div class="block">Validates each proof step for a proof being loaded into mmj.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#getOptFrame()">getOptFrame</a></strong>()</code>
<div class="block">Get the Theorem's OptFrame.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#getProof()">getProof</a></strong>()</code>
<div class="block">Return Theorem's proof.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#isProofStepInExtendedFrame(mmj.lang.Stmt)">isProofStepInExtendedFrame</a></strong>(<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;proofStep)</code>
<div class="block">Checks to see whether or not a proof step is contained in the Theorem's
 Extended Frame.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#loadMandAndOptDjVarsUpdateLists(java.util.Map, java.util.List, java.util.List, java.util.List)">loadMandAndOptDjVarsUpdateLists</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
                               java.util.List&lt;java.util.List&lt;java.lang.String&gt;&gt;&nbsp;inputDjVarsStmtList,
                               java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;mandDjVarsUpdateList,
                               java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;optDjVarsUpdateList)</code>
<div class="block">Utility routine for Theorem Loader to split an input list of Distinct
 Variable statement symbol lists into Mandatory and Optional DjVars lists.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#mergeDjVars(java.util.List, java.util.List)">mergeDjVars</a></strong>(java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;mandDjVarsUpdateList,
           java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;optDjVarsUpdateList)</code>
<div class="block">Merge existing Mandatory and Optional DjVars into the existing Mandatory
 and Optional Frame data.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#proofUpdates(mmj.lang.ParseTree.RPNStep[], mmj.lang.DjVars[], mmj.lang.DjVars[])">proofUpdates</a></strong>(<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;newProof,
            <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;newDjVarsArray,
            <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;newOptDjVarsArray)</code>
<div class="block">Applies updates made to proof related data.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">renderParsedSubExpr</a></strong>(java.lang.StringBuilder&nbsp;sb,
                   int&nbsp;maxDepth,
                   int&nbsp;maxLength,
                   <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;child)</code>
<div class="block">Throws an IllegalArgumentException because a ParseTree for a parsed
 sub-expression should contain only VarHyp and Syntax Axiom nodes.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#replaceDjVars(java.util.List, java.util.List)">replaceDjVars</a></strong>(java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;mandDjVarsUpdateList,
             java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;optDjVarsUpdateList)</code>
<div class="block">Replace existing Mandatory and Optional DjVars.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Theorem.html#setProof(java.util.Map, java.util.List)">setProof</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
        java.util.List&lt;java.lang.String&gt;&nbsp;proofList)</code>
<div class="block">Set Theorem's proof.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.Assrt">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a></h3>
<code><a href="../../mmj/lang/Assrt.html#accumHypInList(java.util.List, T)">accumHypInList</a>, <a href="../../mmj/lang/Assrt.html#getLogHypArray()">getLogHypArray</a>, <a href="../../mmj/lang/Assrt.html#getLogHypArrayLength()">getLogHypArrayLength</a>, <a href="../../mmj/lang/Assrt.html#getLogHypsL1HiLoKey()">getLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Assrt.html#getLogHypsMaxDepth()">getLogHypsMaxDepth</a>, <a href="../../mmj/lang/Assrt.html#getMandFrame()">getMandFrame</a>, <a href="../../mmj/lang/Assrt.html#getMandHypArrayLength()">getMandHypArrayLength</a>, <a href="../../mmj/lang/Assrt.html#getMandVarHypArray()">getMandVarHypArray</a>, <a href="../../mmj/lang/Assrt.html#getSortedLogHypArray()">getSortedLogHypArray</a>, <a href="../../mmj/lang/Assrt.html#isActive()">isActive</a>, <a href="../../mmj/lang/Assrt.html#loadLogHypArray()">loadLogHypArray</a>, <a href="../../mmj/lang/Assrt.html#setLogHypArray(mmj.lang.LogHyp[])">setLogHypArray</a>, <a href="../../mmj/lang/Assrt.html#setMandFrame(mmj.lang.ScopeFrame)">setMandFrame</a>, <a href="../../mmj/lang/Assrt.html#setMandVarHypArray(mmj.lang.VarHyp[])">setMandVarHypArray</a>, <a href="../../mmj/lang/Assrt.html#sortListIntoArray(java.util.List, java.util.Comparator)">sortListIntoArray</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.Stmt">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></h3>
<code><a href="../../mmj/lang/Stmt.html#equals(java.lang.Object)">equals</a>, <a href="../../mmj/lang/Stmt.html#getExprParseTree()">getExprParseTree</a>, <a href="../../mmj/lang/Stmt.html#getExprRPN()">getExprRPN</a>, <a href="../../mmj/lang/Stmt.html#getFormula()">getFormula</a>, <a href="../../mmj/lang/Stmt.html#getLabel()">getLabel</a>, <a href="../../mmj/lang/Stmt.html#getNbrProofRefs()">getNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#getTyp()">getTyp</a>, <a href="../../mmj/lang/Stmt.html#hashCode()">hashCode</a>, <a href="../../mmj/lang/Stmt.html#incrementNbrProofRefs()">incrementNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#initNbrProofRefs()">initNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#resetLogHypsL1HiLoKey()">resetLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#resetLogHypsMaxDepth()">resetLogHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#setExprParseTree(mmj.lang.ParseTree)">setExprParseTree</a>, <a href="../../mmj/lang/Stmt.html#setExprRPN(mmj.lang.ParseTree.RPNStep[])">setExprRPN</a>, <a href="../../mmj/lang/Stmt.html#setLogHypsL1HiLoKey(java.lang.String)">setLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#setLogHypsMaxDepth(int)">setLogHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#setTyp(mmj.lang.Cnst)">setTyp</a>, <a href="../../mmj/lang/Stmt.html#toString()">toString</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#getChapterNbr()">getChapterNbr</a>, <a href="../../mmj/lang/MObj.html#getDescription()">getDescription</a>, <a href="../../mmj/lang/MObj.html#getDescriptionForSearch()">getDescriptionForSearch</a>, <a href="../../mmj/lang/MObj.html#getIsTempObject()">getIsTempObject</a>, <a href="../../mmj/lang/MObj.html#getOrigSectionNbr()">getOrigSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionMObjNbr()">getSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionNbr()">getSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSeq()">getSeq</a>, <a href="../../mmj/lang/MObj.html#setChapterNbr(int)">setChapterNbr</a>, <a href="../../mmj/lang/MObj.html#setDescription(java.lang.String)">setDescription</a>, <a href="../../mmj/lang/MObj.html#setIsTempObject(boolean)">setIsTempObject</a>, <a href="../../mmj/lang/MObj.html#setSectionMObjNbr(int)">setSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#setSectionNbr(int)">setSectionNbr</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="Theorem(int, java.util.List, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Theorem</h4>
<pre>public&nbsp;Theorem(int&nbsp;seq,
       java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;scopeDefList,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
       java.lang.String&nbsp;labelS,
       java.lang.String&nbsp;typS,
       java.util.List&lt;java.lang.String&gt;&nbsp;symList,
       java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
       <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
        throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct Theorem using the entire enchilada from mmj.mmio.SrcStmt.java,
 plus a few condiments.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - MObj.seq sequence number</dd><dd><code>scopeDefList</code> - Scope info in effect at the time</dd><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>stmtTbl</code> - Statement Table (Map)</dd><dd><code>labelS</code> - Theorem label String</dd><dd><code>typS</code> - Theorem Formula Type Code String</dd><dd><code>symList</code> - Theorem Expression Sym String List</dd><dd><code>proofList</code> - Theorem Proof Stmt String List.</dd><dd><code>messages</code> - for error reporting</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if an error occurred</dd><dt><span class="strong">See Also:</span></dt><dd><a href="../../mmj/lang/Theorem.html#editProofListDefAndActive(java.util.Map, java.util.List)"><code>editProofListDefAndActive(Map stmtTbl, List
      proofList)</code></a></dd></dl>
</li>
</ul>
<a name="Theorem(int, java.util.List, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.mmio.BlockList, mmj.lang.ProofCompression, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>Theorem</h4>
<pre>public&nbsp;Theorem(int&nbsp;seq,
       java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;scopeDefList,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
       java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
       java.lang.String&nbsp;labelS,
       java.lang.String&nbsp;typS,
       java.util.List&lt;java.lang.String&gt;&nbsp;symList,
       java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
       <a href="../../mmj/mmio/BlockList.html" title="class in mmj.mmio">BlockList</a>&nbsp;proofBlockList,
       <a href="../../mmj/lang/ProofCompression.html" title="class in mmj.lang">ProofCompression</a>&nbsp;proofCompression,
       <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
        throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct Theorem using the entire enchilada from mmj.mmio.SrcStmt.java
 including compressed proof blocks.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - MObj.seq sequence number</dd><dd><code>scopeDefList</code> - Scope info in effect at the time</dd><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>stmtTbl</code> - Statement Table (Map)</dd><dd><code>labelS</code> - Theorem label String</dd><dd><code>typS</code> - Theorem Formula Type Code String</dd><dd><code>symList</code> - Theorem Expression Sym String List</dd><dd><code>proofList</code> - Theorem Proof Stmt String List.</dd><dd><code>proofBlockList</code> - list containing one or more blocks of compressed
            proof symbols.</dd><dd><code>proofCompression</code> - instance of ProofCompression.java used to
            decompress proof.</dd><dd><code>messages</code> - for error reporting</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if there was a decompression error</dd><dt><span class="strong">See Also:</span></dt><dd><a href="../../mmj/lang/Theorem.html#editProofListDefAndActive(java.util.Map, java.util.List)"><code>editProofListDefAndActive(Map stmtTbl, List
      proofList)</code></a></dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="getProof()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProof</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;getProof()</pre>
<div class="block">Return Theorem's proof.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Theorem's proof.</dd></dl>
</li>
</ul>
<a name="setProof(java.util.Map, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setProof</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;setProof(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
                           java.util.List&lt;java.lang.String&gt;&nbsp;proofList)
                             throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Set Theorem's proof. Updates the Theorem's proof, but only if the proof
 is valid enough to keep -- not saying it is a "valid proof" though :)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>stmtTbl</code> - Statement Table (Map)</dd><dd><code>proofList</code> - Theorem Proof Stmt String List.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Theorem's proof.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if an error occurred</dd><dt><span class="strong">See Also:</span></dt><dd><a href="../../mmj/lang/Theorem.html#editProofListDefAndActive(java.util.Map, java.util.List)"><code>editProofListDefAndActive(Map stmtTbl, List
      proofList)</code></a></dd></dl>
</li>
</ul>
<a name="getOptFrame()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getOptFrame</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;getOptFrame()</pre>
<div class="block">Get the Theorem's OptFrame.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>OptFrame for Theorem.</dd></dl>
</li>
</ul>
<a name="editProofListDefAndActive(java.util.Map, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>editProofListDefAndActive</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;editProofListDefAndActive(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
                                            java.util.List&lt;java.lang.String&gt;&nbsp;proofList)
                                              throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Validates each proof step for a proof being loaded into mmj.
 <p>
 <ol>
 <li>refers to an existing statement label -- or is "?", in which case we
 convert it to "null".
 <li>make sure existing statement label's seq nbr < this stmt seq. (this
 feature has no use when reading a file but when we are adding proofs to
 an existing system we need to make sure we are referring only to earlier
 statements in the database).
 <li>the proof steps are converted from label strings to actual object
 references to existing statements in <code>stmtTbl</code> -- except for
 missing steps denoted by "?", which are converted to "null".
 <li>verify that a step referring to a hypothesis refers to either an
 active hypothesis or an hypothesis in the MandFrame or OptFrame (called
 "Extended Frame" in metamath.pdf.) Note: checking the Frame applies only
 when a proof is being updated after the source file has already been
 loaded -- out of scope, "inactive" hypotheses will be in the Frame if
 they are available for use by the proof!
 <li>as a double-check, if the proofList is empty, raise an exception.
 <li>build the proof array and return it to the caller.
 </ol></div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>stmtTbl</code> - Map of statements already loaded.</dd><dd><code>proofList</code> - Theorem's proof steps, the labels (Strings) of existing
            Stmt's (or "?" for missing step(s)).</dd>
<dt><span class="strong">Returns:</span></dt><dd>RPNStep[] an array of proof steps; contains null entries for
         input proof steps specifying "?" (unknown/missing).</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - (see <code>mmj.lang.LangConstants.java</code>)</dd></dl>
</li>
</ul>
<a name="isProofStepInExtendedFrame(mmj.lang.Stmt)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isProofStepInExtendedFrame</h4>
<pre>public&nbsp;boolean&nbsp;isProofStepInExtendedFrame(<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;proofStep)</pre>
<div class="block">Checks to see whether or not a proof step is contained in the Theorem's
 Extended Frame.
 <p>
 First checks to see if the proof step is in the MandFrame's hypArray. If
 not it checks the OptFrame's hypArray</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofStep</code> - a Statement reference.</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if proof step == a Hyp in either the MandFrame or OptFrame
         of the Theorem.</dd></dl>
</li>
</ul>
<a name="renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>renderParsedSubExpr</h4>
<pre>public&nbsp;int&nbsp;renderParsedSubExpr(java.lang.StringBuilder&nbsp;sb,
                      int&nbsp;maxDepth,
                      int&nbsp;maxLength,
                      <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;child)</pre>
<div class="block">Throws an IllegalArgumentException because a ParseTree for a parsed
 sub-expression should contain only VarHyp and Syntax Axiom nodes.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">renderParsedSubExpr</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>sb</code> - StringBuilder already initialized for appending characters.</dd><dd><code>maxDepth</code> - maximum depth of Notation Syntax axioms in sub-tree to be
            printed. Set to Integer.MAX_VALUE to turn off depth checking.</dd><dd><code>maxLength</code> - maximum length of output sub-expression. Set to
            Integer.MAX_VALUE to turn off depth checking.</dd><dd><code>child</code> - array of ParseNode, corresponding to VarHyp nodes to be
            substituted into the Stmt.</dd>
<dt><span class="strong">Returns:</span></dt><dd>length of sub-expression characters appended to the input
         StringBuilder -- or -1 if maxDepth or maxLength exceeded.</dd></dl>
</li>
</ul>
<a name="proofUpdates(mmj.lang.ParseTree.RPNStep[], mmj.lang.DjVars[], mmj.lang.DjVars[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>proofUpdates</h4>
<pre>public&nbsp;void&nbsp;proofUpdates(<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;newProof,
                <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;newDjVarsArray,
                <a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>[]&nbsp;newOptDjVarsArray)</pre>
<div class="block">Applies updates made to proof related data.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>newProof</code> - previous proof.</dd><dd><code>newDjVarsArray</code> - previous Mandatory DjVars</dd><dd><code>newOptDjVarsArray</code> - previous Optional DjVars</dd></dl>
</li>
</ul>
<a name="loadMandAndOptDjVarsUpdateLists(java.util.Map, java.util.List, java.util.List, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>loadMandAndOptDjVarsUpdateLists</h4>
<pre>public&nbsp;void&nbsp;loadMandAndOptDjVarsUpdateLists(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
                                   java.util.List&lt;java.util.List&lt;java.lang.String&gt;&gt;&nbsp;inputDjVarsStmtList,
                                   java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;mandDjVarsUpdateList,
                                   java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;optDjVarsUpdateList)
                                     throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Utility routine for Theorem Loader to split an input list of Distinct
 Variable statement symbol lists into Mandatory and Optional DjVars lists.
 <p>
 Will throw LangException if both variables not contained in Mandatory or
 Optional Frame hyp arrays!</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - Symbol Table from Logical System.</dd><dd><code>inputDjVarsStmtList</code> - List of lists where the inner list is symList
            from SrcStmt.</dd><dd><code>mandDjVarsUpdateList</code> - empty list upon input to contain the
            Mandatory DjVars generated from the inputDjVarsStmtList.</dd><dd><code>optDjVarsUpdateList</code> - empty list upon input to contain the Optional
            DjVars generated from the inputDjVarsStmtList.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if validation error.</dd></dl>
</li>
</ul>
<a name="replaceDjVars(java.util.List, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>replaceDjVars</h4>
<pre>public&nbsp;void&nbsp;replaceDjVars(java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;mandDjVarsUpdateList,
                 java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;optDjVarsUpdateList)</pre>
<div class="block">Replace existing Mandatory and Optional DjVars.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mandDjVarsUpdateList</code> - List of DjVars object to be stored.</dd><dd><code>optDjVarsUpdateList</code> - List of DjVars object to be stored.</dd></dl>
</li>
</ul>
<a name="mergeDjVars(java.util.List, java.util.List)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>mergeDjVars</h4>
<pre>public&nbsp;void&nbsp;mergeDjVars(java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;mandDjVarsUpdateList,
               java.util.List&lt;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&gt;&nbsp;optDjVarsUpdateList)</pre>
<div class="block">Merge existing Mandatory and Optional DjVars into the existing Mandatory
 and Optional Frame data.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mandDjVarsUpdateList</code> - List of DjVars object to be stored.</dd><dd><code>optDjVarsUpdateList</code> - List of DjVars object to be stored.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Theorem.html" target="_top">Frames</a></li>
<li><a href="Theorem.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#fields_inherited_from_class_mmj.lang.Assrt">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
